s:kl:KndIdLnk fp (IdTop) List, l:IdLnk, tg:Id. sends-on-pair(s;l;tg)   

latex

Definitions	reduce(f;k;as), p  q, p  q, eqof(d), IdLnkDeq, deq-member(eq;x;L), IdDeq, map(f;as), 2of(t), false, 1of(t), (x  l), , x:A. B(x), x. t(x), Knd, IdLnk, Id, Top, a:A fp B(a), t  T, sends-on-pair(s;l;tg)
Lemmas	top wf, Id wf, IdLnk wf, Knd wf, fpf wf, pi1 wf, bfalse wf, bool wf, pi2 wf, map wf, id-deq wf, deq-member wf, idlnk-deq wf, eqof wf, band wf, bor wf, l member wf, reduce wf, list-set-type